"""A parser to handle propositional phrases.

Danny Yoo (dyoo@hkn.eecs.berkeley.edu)

A proposition is an un unevaluated logical expression that can be true
or false, depending on the environment we evaluate one in.

At the moment, I'm reading "The Science Of Programming", by David
Gries.  He has a few chapters on propositional logic, and I got
inspired enough to write a Python program to work with propositional
phrases.

Here are examples of some propositions:

    not X
    x and y and z
    x and y or (x and y)

The last should be interpreted as:

    (x and y) or (x and y)

That is, 'and' should bind more tightly than 'or'.  'not' binds the most
tightly.  That's the sort of knowledge I'll try to build into the parser.

Here's the list of Proposition, in order of increasing precedence.

    Proposition
    EqualityProposition (=, equals)
    ImplicationProposition (->, implies)
    OrProposition (|, or)
    AndProposition (&, and)
    NotProposition (!, not)
    AtomicProposition (T, F)
"""

import spark
import structure
import sys

class ParserError(Exception): pass


def parse(s):
    """Given a string, returns an AST of the parsed expression."""
    import lexer
    p = PropositionParser()
    try:
        tokens = lexer.tokenize(s)
        return p.parse(tokens)
    except spark.ParserError, e:
        raise ParserError, e


class PropositionParser(spark.GenericParser):
    def __init__(self, start='Proposition'):
        spark.GenericParser.__init__(self, start)

    def p_Proposition(self, args):
        ' Proposition ::= AuProposition '
        return args[0]

    def p_AuProposition1(self, args):
        ' AuProposition ::= AuProposition aU EuProposition '
        return structure.AuNode(args[0], args[2])

    def p_AuProposition2(self, args):
        ' AuProposition ::= EuProposition '
        return args[0]

    def p_EuProposition1(self, args):
        ' EuProposition ::= EuProposition eU EqualityProposition '
        return structure.EuNode(args[0], args[2])

    def p_EuProposition2(self, args):
        ' EuProposition ::= EqualityProposition '
        return args[0]

    def p_EqualityProposition1(self, args):
        ''' EqualityProposition ::= EqualityProposition
                                       equals ImplicationProposition '''
        return structure.EqualityNode(args[0], args[2])

    def p_EqualityProposition2(self, args):
        ' EqualityProposition ::= ImplicationProposition '
        return args[0]

    def p_ImplicationProposition1(self, args):
        ''' ImplicationProposition ::= ImplicationProposition
                                          implies OrProposition '''
        return structure.ImplicationNode(args[0], args[2])

    def p_ImplicationProposition2(self, args):
        ' ImplicationProposition ::= OrProposition '
        return args[0]

    def p_OrProposition1(self, args):
        ' OrProposition ::= OrProposition or AndProposition '
        return structure.OrNode(args[0], args[2])

    def p_OrProposition2(self, args):
        ' OrProposition ::= AndProposition '
        return args[0]

    def p_AndProposition1(self, args):
        ' AndProposition ::= AndProposition and EatProposition '
        return structure.AndNode(args[0], args[2])

    def p_AndProposition2(self, args):
        ' AndProposition ::= AatProposition '
        return args[0]

    def p_AatProposition1(self, args):
        ' AatProposition ::= aAT AatProposition '
        return structure.AatNode(args[1])
    
    def p_AatProposition2(self, args):
        ' AatProposition ::= EatProposition '
        return args[0]

    def p_EatProposition1(self, args):
        ' EatProposition ::= eAT EatProposition '
        return structure.EatNode(args[1])
    
    def p_EatProposition2(self, args):
        ' EatProposition ::= NotProposition '
        return args[0]

    def p_NotProposition1(self, args):
        ' NotProposition ::= not NotProposition '
        return structure.NotNode(args[1])

    def p_NotProposition2(self, args):
        ' NotProposition ::= AtomicProposition '
        return args[0]

    def p_atomicProposition1(self, args):
        ' AtomicProposition ::= identifier '
        return structure.IdentifierNode(args[0].attr)

    def p_atomicProposition2(self, args):
        ' AtomicProposition ::= constant '
        value = args[0].attr
        if value == 'tt':
            return structure.TRUE_VALUE
        return structure.FALSE_VALUE

    def p_atomicProposition3(self, args):
        ' AtomicProposition ::= ( Proposition ) '
        return args[1]


def test():
    import prompt
    print """This is a small test of the propositional parser.
Enter propositional phrases at the prompt.  To quit, type "quit" at
the prompt.

Examples of some phrases:

    jack and jill
    rock and rolling implies not moss
"""
    p = prompt.Prompt('ParserTest', callback=_promptCallback)
    p.promptLoop()

def _promptCallback(line):
    try:
        tree = parse(line)
        if tree: print tree
        #print
    except ParserError, e:
        print '''There was a problem parsing your line:\n%s''' % e
        #print
        
if __name__ == '__main__':
    #test()

    line = sys.argv[1]
    _promptCallback(line)

